ds:x:Id fp Type, da:k:Knd fp Type, a:ecl(ds;da), v:ecl-trans-tuple{i:l}(ds;da),
L:event-info(ds;da) List.
(L:event-info(ds;da) List.
(ecl-trans-normal(v) & (n:. ecl-trans-halt2(ds;da;v)(n,L)  (n  ecl-trans-es(v)))
(& (n:.
(& ((L':event-info(ds;da) List. L'  L & ecl-halt(ds;da;a)(n,L'))  ecl-trans-halt2(ds;da;v)(n,L))
(& (m:. ecl-act(ds;da;m;a)(L)  ecl-trans-act(ds;da;v)(m,L)))
 ecl-halt(ds;da;a)(0,L)
 ecl-trans-state(reset-ecl-tuple(v);L)
 =
 ecl-trans-init(reset-ecl-tuple(v))
  ecl-trans-type(reset-ecl-tuple(v)) 

latex

Definitions

x:A. B(x), P  Q, P & Q, , x:A. B(x), AB, {T}, t  T, x. t(x), Prop, A, False, S  T, ij, Top, l1 || l2, P  Q, A & B, ecl-trans-type(A), reset-ecl-tuple(A), ecl-trans-init(v), ecl-trans-h(v), ecl-trans-state-from(v;z;L), Valtype(da;k), let a,b,c,d,e,f,g = u in v(a;b;c;d;e;f;g), list_accum(x,a.f(x;a);y;l), if b t else f fi, 1of(t), false, Y, true, x(s), ecl-trans-halt2(ds;da;A), P  Q, Dec(P), ||as||, b, null(as), P  Q, ecl-trans-tuple{i:l}(ds;da), event-info(ds;da), , Unit,

Lemmas

nat wf, length wf1, non neg length, event-info wf, ecl-trans-tuple wf, ecl wf, fpf wf, Knd wf, Id wf, ecl-halt wf, le wf, ecl-trans-normal wf, nat plus wf, ecl-trans-halt2 wf, nat plus inc, l member wf, ecl-trans-es wf, iff wf, iseg wf, ecl-act wf, ecl-trans-act wf, nat properties, ge wf, iseg weakening, decidable assert, null wf3, top wf, ecl-halt-nil, last lemma, ecl-trans-state-append, reset-ecl-tuple wf, last wf, ecl-trans-type wf, ecl-trans-state wf, ecl-trans-init wf, assert wf, ecl-trans-h wf, ecl-halt-unique, iseg transitivity, iseg append0, member wf, iseg length, length-append, ecl-trans-state-from wf, ecl-reset-state, deq-member wf, Kind-deq wf, bool wf, iff transitivity, eqtt to assert, assert-deq-member, bnot wf, not wf, eqff to assert, assert of bnot, not functionality wrt iff